Theorem 3impia 1118

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 453	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1117	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  mopick2  2637  ceqsalt  3463  3gencl  3473  vtoclgft  3497  rspc6v  3585  mob2  3661  moi  3664  reupick3  4270  disjne  4395  elpr2elpr  4812  disji2  5069  disji  5070  tz7.2  5614  sofld  6151  ordintdif  6374  funopg  6532  fvun1  6931  fvopab6  6982  fveqressseq  7031  fvcofneq  7045  fprg  7109  isores3  7290  ovmpt4g  7514  ovmpos  7515  ov2gf  7516  ofrval  7643  sorpssuni  7686  sorpssint  7687  poxp  8078  poseq  8108  suppss2  8150  frrlem12  8247  smoel  8300  smoord  8305  smogt  8307  oaass  8496  oewordi  8527  oeoalem  8532  oeoelem  8534  nnawordi  8557  nnaass  8558  naddssim  8621  qsel  8743  xpdom3  9013  onsdominel  9064  mapdom3  9087  sdomdomtrfi  9135  domsdomtrfi  9136  php  9141  onomeneq  9148  fisseneq  9173  fodomfir  9238  cantnflem1  9610  ttrclss  9641  cfslbn  10189  cfsmolem  10192  cfcoflem  10194  infpssrlem4  10228  fin23lem7  10238  fin23lem25  10246  isf34lem7  10301  hsmexlem2  10349  axcc3  10360  axdc4lem  10377  tskss  10681  gruss  10719  gruurn  10721  gruiun  10722  gruel  10726  gruen  10735  grudomon  10740  grothac  10753  axpre-sup  11092  axsup  11221  addn0nid  11570  letrp1  11999  p1le  12000  lemul1a  12009  infrelb  12141  nnadddir  12233  zextle  12602  zextlt  12603  btwnnz  12605  gtndiv  12606  uzind2  12622  fzind  12627  zsupss  12887  xrltne  13114  lemaxle  13147  qbtwnre  13151  qbtwnxr  13152  xlemul1a  13240  icogelb  13349  iccleub  13354  iccsplit  13438  uzsubsubfz  13500  elfz0fzfz0  13587  difelfznle  13596  fvffz0  13600  elfzo0le  13658  fzonmapblen  13663  fzofzim  13664  ceile  13808  modadd1  13867  muladdmodid  13872  modmul1  13886  modirr  13904  fsuppmapnn0fiub0  13955  expcl2lem  14035  expclzlem  14045  expnegz  14058  leexp2r  14136  bcval4  14269  bccmpl  14271  hashbnd  14298  hashunsnggt  14356  hashgt23el  14386  hashfundm  14404  elovmpowrd  14520  ccatval2  14540  ccatrcl1  14557  wrdl1s1  14577  ccat2s1fvw  14601  swrdsb0eq  14626  swrdccatin1  14687  pfxccatpfx2  14699  repswswrd  14746  cshwcsh2id  14790  absexpz  15267  climbdd  15634  iseraltlem2  15645  binomfallfac  16006  dvdsle  16279  divalgb  16373  ndvdssub  16378  dvdsgcd  16513  dfgcd2  16515  rplpwr  16527  nn0rppwr  16530  nn0expgcd  16533  lcmgcdlem  16575  lcmfunsn  16613  coprmdvds1  16621  qredeq  16626  2mulprm  16662  prmdvdsexpr  16687  nnnn0modprm0  16777  prm23ge5  16786  pcexp  16830  difsqpwdvds  16858  prmpwdvds  16875  ramcl  17000  cshwshashlem3  17068  cshwrepswhash1  17073  elrestr  17391  mreintcl  17557  mremre  17566  mrieqv2d  17605  initoeu2lem1  17981  funcestrcsetclem9  18114  funcsetcestrclem9  18129  prstr  18265  drsdirfi  18271  latnlej  18422  latnlej2  18425  acsdrsel  18509  acsdrscl  18512  mrelatglb  18526  mrelatlub  18528  isnmgm  18612  grpasscan1  18977  grpinvnz  18986  mulgneg2  19084  gsmsymgrfix  19403  f1omvdco2  19423  symggen  19445  odcl2  19540  odhash3  19551  lsmss1  19640  lsmss2  19642  efgred  19723  efgcpbl  19731  ablfacrp  20043  ablfac1eu  20050  ablfaclem3  20064  omndadd  20103  ogrpaddlt  20113  dvdsrmul1  20349  dvdsunit  20359  irredmul  20409  c0snmgmhm  20442  lmodlema  20860  psgnodpmr  21570  phlssphl  21639  lindsss  21804  lindfmm  21807  ply1scln0  22256  dmatelnd  22461  mdetdiaglem  22563  mdet0  22571  mdetunilem7  22583  slesolinv  22645  cramerimplem3  22650  cpmatpmat  22675  m2cpminvid2lem  22719  chfacfscmul0  22823  chfacfpmmul0  22827  riinopn  22873  clsndisj  23040  cnpf2  23215  hausnei2  23318  cmpcov  23354  cmpfii  23374  unconn  23394  t1connperf  23401  nrmr0reg  23714  fbfinnfr  23806  filuni  23850  alexsubALT  24016  tmdgsum  24060  cuspcvg  24265  mopni  24457  isngp4  24577  metdsre  24819  iimulcl  24904  phtpc01  24963  clmmulg  25068  cfilucfil4  25288  bcthlem5  25295  bcth  25296  bcth3  25298  itg1le  25680  itg2le  25706  bddmulibl  25806  bddiblnc  25809  dvnres  25898  cpnord  25902  dvnfre  25919  deg1ge  26063  dgr1term  26225  aaliou3lem2  26309  sincosq1lem  26461  cxpge0  26647  cxpmul2  26653  logrec  26727  logbgcd1irr  26758  sqfpc  27100  bcmono  27240  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem4  27332  2lgsoddprmlem3  27377  pntrmax  27527  qabvexp  27589  ostth2lem2  27597  nosepon  27629  nolesgn2o  27635  nogesgn1o  27637  nosepnelem  27643  nosepne  27644  nosepdmlem  27647  nosepdm  27648  nodenselem8  27655  noresle  27661  noetasuplem4  27700  noetainflem4  27704  cutbdaylt  27790  eqcuts3  27796  addsuniflem  27993  sltmuls1  28139  precsexlem6  28204  precsexlem7  28205  precsexlem11  28209  ltonold  28253  onnolt  28258  n0fincut  28347  oldfib  28369  expadds  28427  ax5seglem4  29001  axeuclidlem  29031  uhgredgrnv  29199  usgredg4  29286  nbuhgr2vtx1edgblem  29420  vtxduhgr0e  29547  vtxduhgr0nedg  29561  rusgrpropnb  29652  uspgr2wlkeqi  29716  redwlklem  29738  lfgrwlkprop  29754  2pthnloop  29799  spthonepeq  29820  pthdlem2lem  29835  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  crctcshwlkn0lem7  29884  crctcshwlkn0  29889  wlkiswwlks1  29935  wlkiswwlks2  29943  wlkiswwlksupgr2  29945  wwlksnext  29961  wwlksnextproplem2  29978  wspthsnonn0vne  29985  2pthon3v  30011  rusgrnumwwlk  30046  erclwwlkeqlen  30089  erclwwlksym  30091  erclwwlktr  30092  erclwwlkneqlen  30138  erclwwlknsym  30140  erclwwlkntr  30141  uhgr3cyclex  30252  upgreupthseg  30279  eupth2lem3lem4  30301  eucrctshift  30313  4cycl2vnunb  30360  nvs  30734  nvtri  30741  nmlno0  30866  nmlnoubi  30867  ubth  30944  hlipgt0  30985  ocnel  31369  elspansn2  31638  elspansn3  31643  normcan  31647  pjoml2  31682  lecm  31688  osum  31716  nmbdfnlb  32121  leopmul  32205  hstpyth  32300  cvnbtwn  32357  ssmd1  32382  ssmd2  32383  ssdmd1  32384  ssdmd2  32385  cvmd  32407  cvdmd  32408  superpos  32425  disji2f  32647  disjif  32648  disjif2  32651  preiman0  32783  padct  32791  ffs2  32800  bcm1n  32868  sgn3da  32907  s2f1  33005  archiabl  33259  slmdlema  33264  lbslsat  33760  eulerpartlemb  34512  fisshasheq  35297  cvmsdisj  35452  cvmlift2lem12  35496  satfrel  35549  satfrnmapom  35552  fmlasuc  35568  satffun  35591  satef  35598  sategoelfv  35602  lineintmo  36339  nn0prpwlem  36504  nn0prpw  36505  neibastop2lem  36542  tr0elw  36666  lindsadd  37934  areacirc  38034  incsequz  38069  mettrifi  38078  ismtybnd  38128  heiborlem1  38132  rngoisocnv  38302  risci  38308  eqvrelqsel  39021  lfl1  39516  lkrlsp2  39549  omlfh3N  39705  cvrnbtwn  39717  cvrnbtwn2  39721  cvrnbtwn4  39725  cvlexch3  39778  cvlexch4N  39779  cvlatexchb1  39780  2llnne2N  39854  atcvrj0  39874  cvrat2  39875  ps-1  39923  3atlem5  39933  islln2a  39963  lplnriaN  39996  lplnribN  39997  llncvrlpln2  40003  lplncvrlvol2  40061  psubatN  40201  pmapglb2N  40217  pmapglb2xN  40218  2llnma1b  40232  paddasslem17  40282  pmod2iN  40295  pmodl42N  40297  hlmod1i  40302  atmod1i1  40303  atmod1i2  40305  llnmod1i2  40306  pclcmpatN  40347  osumcllem8N  40409  pexmidlem3N  40418  pl42lem4N  40428  4atexlem7  40521  ltrnnid  40582  cdlemc4  40640  cdleme32a  40887  cdlemeg46gfre  40978  cdlemf2  41008  cdlemg4c  41058  trlcoat  41169  tendovalco  41211  tendoeq2  41220  cdlemk36  41359  diael  41489  diatrl  41490  dicelval1stN  41634  dicelval2nd  41635  dihlspsnat  41779  dochkr1  41924  lcfrlem9  41996  mapdh8e  42230  hdmapval0  42279  hgmapval0  42338  dvdsexpnn0  42766  incssnn0  43143  pell14qrexpcl  43295  pell14qrgap  43303  congadd  43394  acongsym  43404  acongtr  43406  dvdsacongtr  43412  jm2.19lem3  43419  jm2.19lem4  43420  jm2.26lem3  43429  onexlimgt  43671  nadd2rabex  43814  ismnushort  44728  bi13impia  44916  3impcombi  45243  ioogtlb  45925  iocgtlb  45932  iocleub  45933  icoltub  45938  iooltub  45940  limclner  46079  limsupre3lem  46160  climuzlem  46171  fsupdm  47270  finfdm  47274  elfzelfzlble  47769  subsubelfzo0  47775  m1modnep2mod  47806  m1modmmod  47812  modlt0b  47817  mod2addne  47818  iccpartigtl  47883  sqrtpwpw2p  48001  fmtnoprmfac1lem  48027  fmtno4prmfac  48035  evenltle  48193  even3prm2  48195  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem1  48281  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  uhgrimisgrgriclem  48406  isubgr3stgrlem7  48448  clnbgr3stgrgrlic  48496  gpgedg2iv  48543  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  upgrwlkupwlk  48616  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797  lincscmcl  48908  lindslinindimp2lem4  48937  lincresunit2  48954  lincresunit3  48957  elfzolborelfzop1  48995  rege1logbzge0  49035  fllog2  49044  dignn0ldlem  49078  rrx2pnecoorneor  49191  rrx2plord2  49198  rrx2linest  49218  ipolub  49463  ipoglb  49466