Theorem 3impia 1116

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 1115	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1088

This theorem is referenced by:  mopick2  2634  ceqsalt  3512  3gencl  3522  vtoclgft  3551  vtoclegft  3587  rspc6v  3642  mob2  3723  moi  3726  reupick3  4335  disjne  4460  elpr2elpr  4873  disji2  5131  disji  5132  tz7.2  5671  sofld  6208  ordintdif  6435  funopg  6601  fvun1  6999  fvopab6  7049  fveqressseq  7098  fvcofneq  7112  fprg  7174  2f1fvneq  7279  isores3  7354  ovmpt4g  7579  ovmpos  7580  ov2gf  7581  ofrval  7708  sorpssuni  7750  sorpssint  7751  poxp  8151  poseq  8181  suppss2  8223  frrlem12  8320  smoel  8398  smoord  8403  smogt  8405  oaass  8597  oewordi  8627  oeoalem  8632  oeoelem  8634  nnawordi  8657  nnaass  8658  naddssim  8721  qsel  8834  xpdom3  9108  onsdominel  9164  mapdom3  9187  sdomdomtrfi  9238  domsdomtrfi  9239  php  9244  onomeneq  9262  fisseneq  9290  fodomfir  9365  cantnflem1  9726  ttrclss  9757  cfslbn  10304  cfsmolem  10307  cfcoflem  10309  infpssrlem4  10343  fin23lem7  10353  fin23lem25  10361  isf34lem7  10416  hsmexlem2  10464  axcc3  10475  axdc4lem  10492  tskss  10795  gruss  10833  gruurn  10835  gruiun  10836  gruel  10840  gruen  10849  grudomon  10854  grothac  10867  axpre-sup  11206  axsup  11333  addn0nid  11680  letrp1  12108  p1le  12109  lemul1a  12118  infrelb  12250  zextle  12688  zextlt  12689  btwnnz  12691  gtndiv  12692  uzind2  12708  fzind  12713  eluzsubOLD  12911  zsupss  12976  xrltne  13201  lemaxle  13233  qbtwnre  13237  qbtwnxr  13238  xlemul1a  13326  icogelb  13434  iccleub  13438  iccsplit  13521  uzsubsubfz  13582  elfz0fzfz0  13669  difelfznle  13678  fvffz0  13682  elfzo0le  13739  fzonmapblen  13744  fzofzim  13745  ceile  13885  modadd1  13944  muladdmodid  13947  modmul1  13961  modirr  13979  fsuppmapnn0fiub0  14030  expcl2lem  14110  expclzlem  14120  expnegz  14133  leexp2r  14210  bcval4  14342  bccmpl  14344  hashbnd  14371  hashunsnggt  14429  hashgt23el  14459  hashfundm  14477  elovmpowrd  14592  ccatval2  14612  ccatrcl1  14628  wrdl1s1  14648  ccat2s1fvw  14672  swrdsb0eq  14697  swrdccatin1  14759  pfxccatpfx2  14771  repswswrd  14818  cshwcsh2id  14863  absexpz  15340  climbdd  15704  iseraltlem2  15715  binomfallfac  16073  dvdsle  16343  divalgb  16437  ndvdssub  16442  dvdsgcd  16577  dfgcd2  16579  rplpwr  16591  nn0rppwr  16594  nn0expgcd  16597  lcmgcdlem  16639  lcmfunsn  16677  coprmdvds1  16685  qredeq  16690  2mulprm  16726  prmdvdsexpr  16750  nnnn0modprm0  16839  prm23ge5  16848  pcexp  16892  difsqpwdvds  16920  prmpwdvds  16937  ramcl  17062  cshwshashlem3  17131  cshwrepswhash1  17136  elrestr  17474  mreintcl  17639  mremre  17648  mrieqv2d  17683  initoeu2lem1  18067  funcestrcsetclem9  18203  funcsetcestrclem9  18218  prstr  18356  drsdirfi  18362  latnlej  18513  latnlej2  18516  acsdrsel  18600  acsdrscl  18603  mrelatglb  18617  mrelatlub  18619  isnmgm  18669  grpasscan1  19031  grpinvnz  19040  mulgneg2  19138  gsmsymgrfix  19460  f1omvdco2  19480  symggen  19502  odcl2  19597  odhash3  19608  lsmss1  19697  lsmss2  19699  efgred  19780  efgcpbl  19788  ablfacrp  20100  ablfac1eu  20107  ablfaclem3  20121  dvdsrmul1  20385  dvdsunit  20395  irredmul  20445  c0snmgmhm  20478  lmodlema  20879  psgnodpmr  21625  phlssphl  21694  lindsss  21861  lindfmm  21864  ply1scln0  22310  dmatelnd  22517  mdetdiaglem  22619  mdet0  22627  mdetunilem7  22639  slesolinv  22701  cramerimplem3  22706  cpmatpmat  22731  m2cpminvid2lem  22775  chfacfscmul0  22879  chfacfpmmul0  22883  riinopn  22929  clsndisj  23098  cnpf2  23273  hausnei2  23376  cmpcov  23412  cmpfii  23432  unconn  23452  t1connperf  23459  nrmr0reg  23772  fbfinnfr  23864  filuni  23908  alexsubALT  24074  tmdgsum  24118  cuspcvg  24325  mopni  24520  isngp4  24640  metdsre  24888  iimulcl  24979  phtpc01  25041  clmmulg  25147  cfilucfil4  25368  bcthlem5  25375  bcth  25376  bcth3  25378  itg1le  25762  itg2le  25788  bddmulibl  25888  bddiblnc  25891  dvnres  25981  cpnord  25985  dvnfre  26004  deg1ge  26151  dgr1term  26313  aaliou3lem2  26399  sincosq1lem  26553  cxpge0  26739  cxpmul2  26745  logrec  26820  logbgcd1irr  26851  sqfpc  27194  bcmono  27335  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  gausslemma2dlem4  27427  2lgsoddprmlem3  27472  pntrmax  27622  qabvexp  27684  ostth2lem2  27692  nosepon  27724  nolesgn2o  27730  nogesgn1o  27732  nosepnelem  27738  nosepne  27739  nosepdmlem  27742  nosepdm  27743  nodenselem8  27750  noresle  27756  noetasuplem4  27795  noetainflem4  27799  scutbdaylt  27877  addsuniflem  28048  ssltmul1  28187  precsexlem6  28250  precsexlem7  28251  precsexlem11  28255  sltonold  28297  ax5seglem4  28961  axeuclidlem  28991  uhgredgrnv  29161  usgredg4  29248  nbuhgr2vtx1edgblem  29382  vtxduhgr0e  29510  vtxduhgr0nedg  29524  rusgrpropnb  29615  uspgr2wlkeqi  29680  redwlklem  29703  lfgrwlkprop  29719  2pthnloop  29763  spthonepeq  29784  pthdlem2lem  29799  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  crctcshwlkn0lem7  29845  crctcshwlkn0  29850  wlkiswwlks1  29896  wlkiswwlks2  29904  wlkiswwlksupgr2  29906  wwlksnext  29922  wwlksnextproplem2  29939  wspthsnonn0vne  29946  2pthon3v  29972  rusgrnumwwlk  30004  erclwwlkeqlen  30047  erclwwlksym  30049  erclwwlktr  30050  erclwwlkneqlen  30096  erclwwlknsym  30098  erclwwlkntr  30099  uhgr3cyclex  30210  upgreupthseg  30237  eupth2lem3lem4  30259  eucrctshift  30271  4cycl2vnunb  30318  nvs  30691  nvtri  30698  nmlno0  30823  nmlnoubi  30824  ubth  30901  hlipgt0  30942  ocnel  31326  elspansn2  31595  elspansn3  31600  normcan  31604  pjoml2  31639  lecm  31645  osum  31673  nmbdfnlb  32078  leopmul  32162  hstpyth  32257  cvnbtwn  32314  ssmd1  32339  ssmd2  32340  ssdmd1  32341  ssdmd2  32342  cvmd  32364  cvdmd  32365  superpos  32382  disji2f  32596  disjif  32597  disjif2  32600  preiman0  32724  padct  32736  ffs2  32745  bcm1n  32802  s2f1  32913  omndadd  33065  ogrpaddlt  33076  archiabl  33187  slmdlema  33191  lbslsat  33643  eulerpartlemb  34349  sgn3da  34522  fisshasheq  35098  cvmsdisj  35254  cvmlift2lem12  35298  satfrel  35351  satfrnmapom  35354  fmlasuc  35370  satffun  35393  satef  35400  sategoelfv  35404  lineintmo  36138  nn0prpwlem  36304  nn0prpw  36305  neibastop2lem  36342  lindsadd  37599  areacirc  37699  incsequz  37734  mettrifi  37743  ismtybnd  37793  heiborlem1  37797  rngoisocnv  37967  risci  37973  eqvrelqsel  38597  lfl1  39051  lkrlsp2  39084  omlfh3N  39240  cvrnbtwn  39252  cvrnbtwn2  39256  cvrnbtwn4  39260  cvlexch3  39313  cvlexch4N  39314  cvlatexchb1  39315  2llnne2N  39390  atcvrj0  39410  cvrat2  39411  ps-1  39459  3atlem5  39469  islln2a  39499  lplnriaN  39532  lplnribN  39533  llncvrlpln2  39539  lplncvrlvol2  39597  psubatN  39737  pmapglb2N  39753  pmapglb2xN  39754  2llnma1b  39768  paddasslem17  39818  pmod2iN  39831  pmodl42N  39833  hlmod1i  39838  atmod1i1  39839  atmod1i2  39841  llnmod1i2  39842  pclcmpatN  39883  osumcllem8N  39945  pexmidlem3N  39954  pl42lem4N  39964  4atexlem7  40057  ltrnnid  40118  cdlemc4  40176  cdleme32a  40423  cdlemeg46gfre  40514  cdlemf2  40544  cdlemg4c  40594  trlcoat  40705  tendovalco  40747  tendoeq2  40756  cdlemk36  40895  diael  41025  diatrl  41026  dicelval1stN  41170  dicelval2nd  41171  dihlspsnat  41315  dochkr1  41460  lcfrlem9  41532  mapdh8e  41766  hdmapval0  41815  hgmapval0  41874  nnadddir  42283  dvdsexpnn0  42347  incssnn0  42698  pell14qrexpcl  42854  pell14qrgap  42862  congadd  42954  acongsym  42964  acongtr  42966  dvdsacongtr  42972  jm2.19lem3  42979  jm2.19lem4  42980  jm2.26lem3  42989  onexlimgt  43231  nadd2rabex  43375  ismnushort  44296  bi13impia  44485  3impcombi  44814  ioogtlb  45447  iocgtlb  45454  iocleub  45455  icoltub  45460  iooltub  45462  limclner  45606  limsupre3lem  45687  climuzlem  45698  fsupdm  46797  finfdm  46801  elfzelfzlble  47270  subsubelfzo0  47275  m1modnep2mod  47291  iccpartigtl  47347  sqrtpwpw2p  47462  fmtnoprmfac1lem  47488  fmtno4prmfac  47496  evenltle  47641  even3prm2  47643  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem1  47729  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  uhgrimisgrgriclem  47835  isubgr3stgrlem7  47874  clnbgr3stgrgrlic  47914  upgrwlkupwlk  47983  funcringcsetcALTV2lem9  48141  funcringcsetclem9ALTV  48164  lincscmcl  48277  lindslinindimp2lem4  48306  lincresunit2  48323  lincresunit3  48326  elfzolborelfzop1  48364  m1modmmod  48370  rege1logbzge0  48408  fllog2  48417  dignn0ldlem  48451  rrx2pnecoorneor  48564  rrx2plord2  48571  rrx2linest  48591  ipolub  48776  ipoglb  48779